FDL - Nuprl Lemma : assert-eq-knd

Nuprl Lemma : assert-eq-knd

a,b:Knd. (

eq_knd(a; b))

(a = b)

Definitions x:A. B(x), P Q, eq_knd(a; b), P Q, prop{i:l}, P Q, t T, P Q

Lemmas iff functionality wrt iff, assert wf, eqof wf, Kind-deq wf, deq property, Knd wf